<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- NewPage -->
<html lang="en">
<head>
<title>MMTTheoremExportFormatter</title>
<link rel="stylesheet" type="text/css" href="../../stylesheet.css" title="Style">
</head>
<body>
<script type="text/javascript"><!--
    if (location.href.indexOf('is-external=true') == -1) {
        parent.document.title="MMTTheoremExportFormatter";
    }
//-->
</script>
<noscript>
<div>JavaScript is disabled on your browser.</div>
</noscript>
<!-- ========= START OF TOP NAVBAR ======= -->
<div class="topNav"><a name="navbar_top">
<!--   -->
</a><a href="#skip-navbar_top" title="Skip navigation links"></a><a name="navbar_top_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/tl/MMTFolder.html" title="class in mmj.tl"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/tl/MMTTheoremFile.html" title="class in mmj.tl"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/tl/MMTTheoremExportFormatter.html" target="_top">Frames</a></li>
<li><a href="MMTTheoremExportFormatter.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_top">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_top");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_top">
<!--   -->
</a></div>
<!-- ========= END OF TOP NAVBAR ========= -->
<!-- ======== START OF CLASS DATA ======== -->
<div class="header">
<div class="subTitle">mmj.tl</div>
<h2 title="Class MMTTheoremExportFormatter" class="title">Class MMTTheoremExportFormatter</h2>
</div>
<div class="contentContainer">
<ul class="inheritance">
<li>java.lang.Object</li>
<li>
<ul class="inheritance">
<li>mmj.tl.MMTTheoremExportFormatter</li>
</ul>
</li>
</ul>
<div class="description">
<ul class="blockList">
<li class="blockList">
<hr>
<br>
<pre>public class <span class="strong">MMTTheoremExportFormatter</span>
extends java.lang.Object</pre>
<div class="block">Converts a thing into a list Metamath-formatted file lines.
 <p>
 The output Metamath .mm file text lines are formatted according to the
 Theorem Loader Preferences.
 <p>
 Note: output lines do not contain newlines.
 <p>
 Note: this code handles Theorems and ProofWorksheets, and in theory there
 could be subclasses involved, but it seemed ok to just put all of the
 formatting code in one spot here as a quick and dirty bit of coding.</div>
</li>
</ul>
</div>
<div class="summary">
<ul class="blockList">
<li class="blockList">
<!-- ======== CONSTRUCTOR SUMMARY ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_summary">
<!--   -->
</a>
<h3>Constructor Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Constructor Summary table, listing constructors, and an explanation">
<caption><span>Constructors</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colOne" scope="col">Constructor and Description</th>
</tr>
<tr class="altColor">
<td class="colOne"><code><strong><a href="../../mmj/tl/MMTTheoremExportFormatter.html#MMTTheoremExportFormatter(mmj.tl.TlPreferences)">MMTTheoremExportFormatter</a></strong>(<a href="../../mmj/tl/TlPreferences.html" title="class in mmj.tl">TlPreferences</a>&nbsp;tlPreferences)</code>
<div class="block">Basic constructor.</div>
</td>
</tr>
</table>
</li>
</ul>
<!-- ========== METHOD SUMMARY =========== -->
<ul class="blockList">
<li class="blockList"><a name="method_summary">
<!--   -->
</a>
<h3>Method Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Method Summary table, listing methods, and an explanation">
<caption><span>Methods</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier and Type</th>
<th class="colLast" scope="col">Method and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code>java.util.List&lt;java.lang.StringBuilder&gt;</code></td>
<td class="colLast"><code><strong><a href="../../mmj/tl/MMTTheoremExportFormatter.html#buildStringBuilderLineList(mmj.pa.ProofWorksheet)">buildStringBuilderLineList</a></strong>(<a href="../../mmj/pa/ProofWorksheet.html" title="class in mmj.pa">ProofWorksheet</a>&nbsp;proofWorksheet)</code>
<div class="block">Converts a ProofWorksheet into a list of StringBuilder lines formatted
 into Metamath format.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>java.util.List&lt;java.lang.StringBuilder&gt;</code></td>
<td class="colLast"><code><strong><a href="../../mmj/tl/MMTTheoremExportFormatter.html#buildStringBuilderLineList(mmj.lang.Theorem)">buildStringBuilderLineList</a></strong>(<a href="../../mmj/lang/Theorem.html" title="class in mmj.lang">Theorem</a>&nbsp;theorem)</code>
<div class="block">Converts a Theorem in the LogicalSystem into a list of StringBuilder
 lines formatted into Metamath format.</div>
</td>
</tr>
</table>
<ul class="blockList">
<li class="blockList"><a name="methods_inherited_from_class_java.lang.Object">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;java.lang.Object</h3>
<code>clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait</code></li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
<div class="details">
<ul class="blockList">
<li class="blockList">
<!-- ========= CONSTRUCTOR DETAIL ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_detail">
<!--   -->
</a>
<h3>Constructor Detail</h3>
<a name="MMTTheoremExportFormatter(mmj.tl.TlPreferences)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>MMTTheoremExportFormatter</h4>
<pre>public&nbsp;MMTTheoremExportFormatter(<a href="../../mmj/tl/TlPreferences.html" title="class in mmj.tl">TlPreferences</a>&nbsp;tlPreferences)</pre>
<div class="block">Basic constructor.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>tlPreferences</code> - TlPreferences object.</dd></dl>
</li>
</ul>
</li>
</ul>
<!-- ============ METHOD DETAIL ========== -->
<ul class="blockList">
<li class="blockList"><a name="method_detail">
<!--   -->
</a>
<h3>Method Detail</h3>
<a name="buildStringBuilderLineList(mmj.lang.Theorem)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>buildStringBuilderLineList</h4>
<pre>public&nbsp;java.util.List&lt;java.lang.StringBuilder&gt;&nbsp;buildStringBuilderLineList(<a href="../../mmj/lang/Theorem.html" title="class in mmj.lang">Theorem</a>&nbsp;theorem)</pre>
<div class="block">Converts a Theorem in the LogicalSystem into a list of StringBuilder
 lines formatted into Metamath format.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>theorem</code> - Theorem in the Logical System.</dd>
<dt><span class="strong">Returns:</span></dt><dd>LinkedList of StringBuilder objects each containing one line of
         text in Metamath-format (without newlines.)</dd></dl>
</li>
</ul>
<a name="buildStringBuilderLineList(mmj.pa.ProofWorksheet)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>buildStringBuilderLineList</h4>
<pre>public&nbsp;java.util.List&lt;java.lang.StringBuilder&gt;&nbsp;buildStringBuilderLineList(<a href="../../mmj/pa/ProofWorksheet.html" title="class in mmj.pa">ProofWorksheet</a>&nbsp;proofWorksheet)
                                                                   throws <a href="../../mmj/lang/TheoremLoaderException.html" title="class in mmj.lang">TheoremLoaderException</a></pre>
<div class="block">Converts a ProofWorksheet into a list of StringBuilder lines formatted
 into Metamath format.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>proofWorksheet</code> - ProofWorksheet object</dd>
<dt><span class="strong">Returns:</span></dt><dd>LinkedList of StringBuilder objects each containing one line of
         text in Metamath-format (without newlines.)</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/TheoremLoaderException.html" title="class in mmj.lang">TheoremLoaderException</a></code> - if the ProofWorksheet is null or is not
             unified.</dd></dl>
</li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
</div>
<!-- ========= END OF CLASS DATA ========= -->
<!-- ======= START OF BOTTOM NAVBAR ====== -->
<div class="bottomNav"><a name="navbar_bottom">
<!--   -->
</a><a href="#skip-navbar_bottom" title="Skip navigation links"></a><a name="navbar_bottom_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/tl/MMTFolder.html" title="class in mmj.tl"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/tl/MMTTheoremFile.html" title="class in mmj.tl"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/tl/MMTTheoremExportFormatter.html" target="_top">Frames</a></li>
<li><a href="MMTTheoremExportFormatter.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_bottom">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_bottom");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_bottom">
<!--   -->
</a></div>
<!-- ======== END OF BOTTOM NAVBAR ======= -->
</body>
</html>
